<%@ page contentType="text/html; charset=gb2312" language="java" import="java.io.*,java.util.*,GSR.web.*,com.maplesoft.externalcall.*,com.maplesoft.openmaple.*" errorPage="" %>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<%
		 String statement= request.getParameter("statement"); 
		 String system = request.getParameter("system");
		 //out.println(name);
		 //out.println(statement);
		 //out.println(system);
		 Vector<String> H = Utility.generateTermSet(statement);
		 out.println("<h5>The problem of " + H.get(1) +" is tansformed into native representations in GEOTHER: </h5>");
		 CallBacks callback = new CallBacks();
		 Engine engine = Utility.buildEngine4Maple(callback);
		 Prove prove = new Prove(H.get(1),statement,system,engine,callback);
		 out.println(prove.getNativeRepresentations());
		 out.println("<h5>Proof of " + H.get(1) +" in GEOTHER</h5>");
		 out.println(prove.getHtmlOfProof());
		 prove.getEngine().stop();

%>
